COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∂29-Sep-87  1644	VAL  	Ramification  
C00005 ENDMK
C⊗;
∂29-Sep-87  1644	VAL  	Ramification  
To:   JMC@SAIL.STANFORD.EDU, SJG@SAIL.STANFORD.EDU,
      de2smith@SCORE.STANFORD.EDU, shoham@SCORE.STANFORD.EDU

The formalization of the blocks world in my paper on theories of action has
this flaw: in addition to

(holds(at(b,l1),s) and holds(at(b,l2),s)) implies (l1 equals l2)            (1)

and

causes(move(b,l),at(b,l),true)						    (2)

I had to postulate

not (l equals l1) implies causes(move(b,l),at(b,l1),false).		    (3)

This is an example of the "ramification problem": (3) must be a
"ramification" of (1) and (2), it shouldn't be necessary to state it as an
additional axiom. The following trick seems to solve the problem (at least
in this case).

We introduce another predicate, causes1, for "intrastate" causality. It takes
4 arguments; causes1(f,v,f',v') expresses that the fluent f getting the value
v causes the fluent f' to get the value v'. For instance, we can postulate:

not (l equals l1) implies causes1(at(b,l),true,at(b,l1),false).             (4)

The new predicate causes1 will be circumscribed, along with causes and precond.
The following general axioms relate causes1 to other predicates:

(causes1(f,v,f',v') and (val(f,s) equals v)) implies (val(f',s) equals v'), (5)

(causes(a,f,v) and causes1(f,v,f',v')) implies causes(a,f',v').             (6)

In the presence of these general axioms and (2), we can replace (1) and (3) by one
axiom (4). Both (1) and (3) will follow; for the former, we'll need to
view holds(f,s) as an abbreviation for: val(f,s) equals true.

What do you think? If you like this idea, maybe you'll suggest better names than
"causes" and "causes1".

Vladimir